(*<br>

<font color="red"><b>This is SERE.ml.html which is SERE.ml with HTML markup hidden in ML comments.</b></font>
<html>
<head>
<title>SERE.ml.html</title>
<!-- IE, but not Firebird, seems to collapse whitespace inside divs, 
     so I added <pre> </pre> for each one. Yuk!
     I tried adding a property "whitespace: pre;" to the style-sheets,
     but it didn't work. Do you know a better solution for IE?
-->
<style type="text/css">
 div.comment {background: rgb(221,221,221);
              color: black;
              width: 190mm;
              border: groove red;}
</style>
<style type="text/css">
 div.session {background: rgb(204,255,255);
              color: blue;
              width: 98%;
              margin-top:5px;
              margin-bottom:5px;
              margin-left:5px;
              margin-right:5px;
              border: thin dotted blue;}
</style>
<body bgcolor="white"><pre>*)




(*****************************************************************************)
(* Simple example encoding part of Johan Martensson's April 15, 2004 message *)
(* (with changes for fusion from later messages, and proof hints from Johan) *)
(*                                                                           *)
(* UPDATES:                                                                  *)
(* END changed by Johan Martensson Mon Apr 26 2004                           *)
(* Explanation of HOL commands added by MJCG: started work on May 6, 2004    *)
(* Made tweaks suggested by Konrad Slind Thu Jun 24, 2004                    *)
(*****************************************************************************)

(*<div class="comment"><pre>Comments in this kind of light gray box explain the ML and HOL
commands in this file. The idea is to have a kind of 'bottom up'
tutorial that complements the more 'top down' approach of the main
tutorial at: <a href="http://cvs.sourceforge.net/viewcvs.py/hol/hol98/Manual/Tutorial/">http://cvs.sourceforge.net/viewcvs.py/hol/hol98/Manual/Tutorial/</a>
</pre></div>*)

(*<div class="comment"><pre>
This file (SERE.ml.html) is not intended for separate compilation using
Holmake, but is intended to be input with the ML command <font color="blue">use</font>. 

When HOL is run from a shell, an ml file can be given to customise the
session.  For example, I always run with a customisation file
<font color="blue">preface.ml</font>, as illustrated in the session below (for improved
readability I'll enclose sessions between opening and closing HTML
div-tags with a class attribute "session" which I'll set to display on
a light blue/green background). For example, starting in Linux (shell
prompt is <font color="blue">%</font>) I would run:
<div class="session"><pre>
% hol.unquote /local/scratch-1/mjcg/HOL98/preface.ml

-----------------------------------------------------------------
       HOL-4 [Kananaskis 2 (built Thu Jan 29 13:10:13 2004)]

       For introductory HOL help, type: help "hol";
-----------------------------------------------------------------

[loading HOL power tools ************* ]
[closing file "/local/scratch-1/mjcg/HOL98/hol98/tools/end-init-boss.sml"]
- 
</pre></div>This file is then loaded as follows (continuing in the HOL session
just started):
<div class="session"><pre>
- use "SERE.ml.html";
[opening file "/tmp/file7F00zl.hol"]
&lt;&lt;HOL message: intLib loaded.  
Use intLib.deprecate_int() to turn off integer parsing>>
> val it = () : unit
&lt;&lt;HOL message: Defined type: "A">>;
> val A_def = () : unit
> val A_11 =
    |- (!a a'. (N a = N a') = (a = a')) /\ !a a'. (W a = W a') = (a = a') : thm
  val A_distinct = |- !a' a. ~(N a = W a') : thm

... lots of stuff deleted ...

> val TightPrefix =
    |- !r w. US_SEM w r ==> !u. STRICT_PREFIX u w ==> US_SEM (WEAKEN u) r : thm
[closing file "/tmp/file7F00zl.hol"]
</pre></div>I have deleted most of the output from HOL in this example. In
examples of interaction with HOL I may make small edits to improve the
appearance (e.g. I added a line-break after <font color="blue">&lt;&lt;HOL message: intLib loaded.</font> 
in the output above.)

So that this file works anywhere, I include the definitions in my
startup file <font color="blue">preface.ml</font>. The first definition just increases an ML
variable called <font color="blue">delayLines</font>. Documentation is available via the ML
help system, as illustrated by:<div class="session"><pre>
- help "displayLines";

... stuff deleted ...

@>   [displayLines] is a reference to the size of the display (window)
+    assumed by the defaultBrowser; initially 24 lines.  Set it to the
+    actual size of your window for best results.  
</pre></div>
Set <font color="blue">displayLines</font> to 10000 because the default (40 or so) parcels out the 
information in a "more" like fashion (page at a time). Setting the limit high 
is better for emacs.
</pre></div>*)
displayLines := 10000;
(*<div class="comment"><pre>
The ML function <font color="blue">prove_thm</font>, defined below, has the same ML type as the
built in function <font color="blue">store_thm</font>, but it doesn't actually save the
theorem in the current theory. It also prints out the time taken to
execute the tactic, since <font color="blue">prove</font> doesn't. I defined this so that I
could easily edit occurrences of <font color="blue">store_theorem</font> (which saves theorems
in the current theory with the name given as a string as the first
argument) to something that wouldn't clutter up the theory file with
results that were either not used or I subsequently decided were not
worth saving.
</pre></div>*)
fun prove_thm(_:string,tm,tac) = time prove (tm,tac);

(*<div class="comment"><pre>
Modify <font color="blue">store_thm</font> to print out proof times.

To see what <font color="blue">time</font> does, apply the ML function <font color="blue">help</font> to the string
<font color="blue">"time"</font>, and then select option 7 by typing <font color="blue">"7"</font>.
</pre></div>*)
val store_thm = fn (str,tm,tac) => time store_thm (str,tm,tac);

(*<div class="comment"><pre>
The next declaration defines an ML shortcut function <font color="blue">g</font> to set a new
goal (for interactive proof) with no assumptions. Will illustrate
interactive proof later.
</pre></div>*)
fun g tm = set_goal([],tm);

(*<div class="comment"><pre>
ML function to toggle the value of the ML variable <font color="blue">show_types</font> that
determines whether HOL types are printed or not. Here's an example:
<div class="session"><pre>
- ``z = x < y``; 
> val it = ``z = x < y`` : term
- ty();
> val it = true : bool
- ``z = x < y``;
> val it = ``(z :bool) = (x :num) < (y :num)`` : term
- ty();
> val it = false : bool
- ``z = x < y``;
> val it = ``z = x < y`` : term</pre></div></pre></div>*)
fun ty() = let val ty_val = !show_types in
  (show_types := not ty_val;
   not ty_val)
 end;
(*<div class="comment"><pre>
The function <font color="blue">db</font> defined below is used to search for existing
theorems matching a term. The structure <font color="blue">DB</font> contains various functions
for accessing the HOL database of theories. Use <font color="blue">help</font> to see the
list of what is available in <font color="blue">DB</font>.  </pre></div>*) 
val db = DB.match [];

(*<div class="comment"><pre>
This concludes the commentary of the preface file I use. 

Now we start the commands. The first bunch of stuff loads the
structures <font color="blue">intLib</font> (various arithmetical definitions and theorems,
including negative numbers -- HOL's default is just the naturals),
<font color="blue">Cooper</font> (a presberger decision procedure tool) and <font color="blue">rich_listTheory</font>
(miscellaneous definitions and theorem about lists.

Including ML commands between  <font color="blue">quietdec := true;</font> and <font color="blue">quietdec := false;</font>
stops (most of) the output from being printed.

Opening <font color="blue">intLib</font> changes the default numerical type to be ``:int``, the
integers (positive and negative numbers). We want the default to be reset to
natural numbers, which is done by evaluating <font color="blue">intLib.deprecate_int();</font>.

Opening a structure (e.g. a theory) binds all the ML names in the
structure to the corresponding values.
</pre></div>*)

(*****************************************************************************)
(* Load in useful stuff                                                      *)
(*****************************************************************************)
quietdec := true;                         (* Switch off output               *)
map load 
 ["intLib", "Cooper","rich_listTheory"];  (* Load useful theories            *)
intLib.deprecate_int();                   (* Set num as default numbers type *)
open rich_listTheory;                     (* Open theories                   *)
quietdec := false;                        (* Restore output                  *)

(*****************************************************************************)
(* N^f = { w | w is a finite list of states/letters } (the set of neutral    *)
(* finite words)                                                             *)
(*                                                                           *)
(* we let \epsilon be the empty (neutral) word                               *)
(*                                                                           *)
(* W = { W(w) | w \in N^f } (the set of weak finite words)                   *)
(*                                                                           *)
(* Let A = N^f U W                                                           *)
(*****************************************************************************)

(*<div class="comment"><pre>
The definition of <font color="blue">A_def</font> below is an ML value binding of the form:

 <font color="blue">val <i>name</i> = HOL_datatype `<i>description of datatype</i>`;</font>

<font color="blue">HOL_datatype</font> is a HOL tool (an ML function) that takes a
specification of a datatype and make a type definition that implements
the specification. Various theorems are automatically proved and saved
in the database (structure <font color="blue">DB</font>). Examples include structural induction
theorems, the injectiveness (i.e. one-to-one) nature of the
constructors, and the distinctness of the constructors. Various proof
tools can then automatically use these definitional axioms.

My convention is to name (in ML) the result of a definition with a
string obtained by concatenationg <font color="blue">_def</font> the thing (type or
constant) being defined. In the case of a type definition, the
definitional axioms are secreted away in the DB structure, and
HOL_datatype returns <font color="blue">()</font> (i.e. it is a pure side-effect), so this
naming is vacuous. However, it makes more sense for constants (see
below). When a file is separately compiled it needs to consist only of
ML declarations, thus expressions executed only for their side-effects
have to be wrapped up as a dummy declaration.  Thus, when this
file is tweaked to be compilable the <font color="blue">val A_def = ...</font> will be
essential (this is a messy feature of Moscow ML compilation).

In the ML representation of higher order logic there is an initially
confusing distinction between singly-quoted terms like <font color="blue">`x+1`</font> and
doubly quoted terms like <font color="blue">``x+1``</font>. The difference is a bit tricky and
(IMHO) ad hoc. Roughly: singly quoted terms are not fully parsed and
type checked, but doubly quoted terms are. Note that doubly-quoted
terms require one to be using <font color="blue">hol.unquote</font> rather than just <font color="blue">hol</font>.

ML functions that need to supply a type-checking context take singly
quoted terms (which have ML type <font color="blue">term frag list</font>), but functions that
need a fully type-checked term take doubly-quoted terms (which have ML
type <font color="blue">term</font>).

There is a similar distinction between singly and doubly quoted types
of higher order logic (e.g. <font color="blue">`:num`</font> and <font color="blue">``:num``</font>, respectively). 
Singly quoted types are ML values with ML type <font color="blue">hol_type frag list</font>
and doubly quoted types are ML values with type <font color="blue">hol_type</font>.

I think it is best not to worry about this
object-languate/meta-language stuff initially, but one does need to
know which functions require singly quoted arguments and which require
double quoted.

The function <font color="blue">HOL_datatype</font> for defining datatypes requires a singly
quoted type and the function <font color="blue">Define</font> for defining constants requires
a singly quoted term.
</pre></div>*)

(*****************************************************************************)
(* Here is a datatype definition of a type A (hopefully self-explanatory).   *)
(* It creates a tagged disjoint union with elements ``N l`` and ``W l``,     *)
(* where l is a HOL list (a pre-defined datatype).                           *)
(*****************************************************************************)
val A_def =
 Hol_datatype
  `A = N of 'a list
     | W of 'a list`;

(*<div class="comment"><pre>
The result of executing the datatype declaration above is to extend
the current theory with a new type <font color="blue">``:'a A``</font> which is isomorphic to
the disjoint union of two copies of the type <font color="blue">``:'a list``</font> of lists
(which is predefined when HOL is built). Here, as in ML, <font color="blue">'a</font> is a type
variable (<font color="blue">``:bool list``</font> is the type of boolean lists, and <font color="blue">``:num list``</font>
the type of lists of natural numbers).

The datatype <font color="blue">``:'a A``</font> is equipped with constructors, which are HOL
constants with types:

 <font color="blue">N : 'a list -> 'a A</font>
 <font color="blue">W : 'a list -> 'a A</font>

These constructors 'tag' the lists in the disjoint union. Amongst the
definitional axioms that define the type are the <font color="blue">A_11</font> and
<font color="blue">A_distinct</font> declared below by using the ML function assoc to extract
from the automatically created database. All the axioms associated
with type <font color="blue">``:'a A``</font> can be seen by applying <font color="blue">DB.theorems</font> to the name
of the current theory, which, by default, is <font color="blue">"-"</font> (we could have
declared a more mnemonic name).
<div class="session"><pre>
DB.theorems "-";
> val it =
    [("A_11",
      |- (!a a'. (N a = N a') = (a = a')) /\ !a a'. (W a = W a') = (a = a')),
     ("A_distinct", |- !a' a. ~(N a = W a')),
     ("A_case_cong",
      |- !M M' f f1.
           (M = M') /\ (!a. (M' = N a) ==> (f a = f' a)) /\
           (!a. (M' = W a) ==> (f1 a = f1' a)) ==>
           (case f f1 M = case f' f1' M')),
     ("A_nchotomy", |- !A. (?l. A = N l) \/ ?l. A = W l),
     ("A_Axiom", |- !f0 f1. ?fn. (!a. fn (N a) = f0 a) /\ !a. fn (W a) = f1 a),
     ("A_induction", |- !P. (!l. P (N l)) /\ (!l. P (W l)) ==> !A. P A)] :
  (string * thm) list</pre></div></pre></div>*)

(*****************************************************************************)
(* Retrieve from data-base (DB) automatically proved theorems about A        *)
(*****************************************************************************)
val A_11       = assoc "A_11"       (DB.theorems "-")
and A_distinct = assoc "A_distinct" (DB.theorems "-");

(*<div class="comment"><pre>
The following ML declaration uses the function <font color="blue">Define</font> that delares a
new HOL constant named <font color="blue">ELEM</font> in terms of an existing constant
<font color="blue">EL</font>. Define takes a singly quoted term consisting of a conjunction of
equations (or a single equation) and tries to define a constant that
satisfies the equations. This uses the TFL technology developed by
Konrad Slind as part of his PhD work at Munich. The idea of TFL is to
support 'ML-like' definitions and to automatically prove they
terminate.

A term <font color="blue">``ELEM a n``</font> evaluates the nth element (starting from 0) of
<font color="blue">``a``</font> (a value of type <font color="blue">``:'a A``</font>). It splits on the two possible cases
for <font color="blue">``a``</font> and then  invokes <font color="blue">``EL n``</font> on the list representing <font color="blue">``a``</font>.
</pre></div>*)
val ELEM_def =
 Define
  `(ELEM (N l) n = EL n l) 
   /\
   (ELEM (W l) n = EL n l) `;

(*****************************************************************************)
(* We define concatenation ( * ) on A: if v,w \in N then v*w is just the     *)
(* list concatenation of v and w (remember v,w finite) v*W(w) = W(v*w)       *)
(* and for v\in W and w\in A v*w = v                                         *)
(*****************************************************************************)

(*****************************************************************************)
(* For readability overload "++" onto HOL's list append constant APPEND,     *)
(* and make it a left associative infix with precedence 500.                 *)
(*****************************************************************************)
set_fixity "++" (Infixl 500);
overload_on("++", ``APPEND``);

(*****************************************************************************)
(* Define ``CONC`` for concatenation on values of type A.                    *)
(*****************************************************************************)
set_fixity "CONC" (Infixl 500);

val CONC_def =
 Define
  `(N v CONC N w = N(v++w))
   /\
   (N v CONC W w = W(v++w))
   /\
   (W v CONC a   = W v)`;

(*****************************************************************************)
(* Overload "*" on to "CONC" for readability.                                *)
(*****************************************************************************)
overload_on("*", ``$CONC``);

(*<div class="comment"><pre>
The ML definition of <font color="blue">CONC_identity</font> below proves a theorem using the
HOL function <font color="blue">prove</font>, which takes a (doubly-quoted) term and a tactic,
applies the tactic to the term, and if the tactic proves the desired
theorem, a value of ML type <font color="blue">thm</font> is returned. The only way to create
values of type <font color="blue">thm</font> is to perform a sequence of inference steps on
axioms (logical or definitional). A tactic is an ML function that
decomposes a goal, and as it does so builds up a sequence of proof
steps to create the theorem from the axioms.

In this file, tactics are given as a single ML expressions built out
of primitive tactics using 'tacticals', like the ML infix
<font color="blue">THEN</font>. However, these tactics are created interactively, using a goal
management tool.

The session below shows an interactive proof of <font color="blue">CONC_identity</font>.  The
following ML functions are used:

 1. <font color="blue">g</font> -- starts a new interactive proof session given a goal

 2. <font color="blue">e</font> -- applies a tactic to the goal on the top of the goal stack

 3. <font color="blue">Cases_on `a`</font> -- does a case-split on <font color="blue">`a`</font>

 4. <font color="blue">RW_TAC list_ss [CONC_def]</font> -- rewrites using the standard list
    rewriting simplification set (<font color="blue">list_ss</font>) and the definition of <font color="blue">CONC</font>.
<div class="session"><pre>
g ``(N[] * a = a) /\ (a * N[] = a)``;                         <font color="red">(* Set up goal *)</font>
&lt;&lt;HOL message: inventing new type variable names: 'a>>
> val it =
    Proof manager status: 1 proof.
    1. Incomplete:
         Initial goal:
         (N [] * a = a) /\ (a * N [] = a)

     : proofs

- e (Cases_on `a`);                       <font color="red">(* Expand goal by doing cases on a *)</font>
OK..
2 subgoals:
> val it =
    (N [] * W l = W l) /\ (W l * N [] = W l)
    
    
    (N [] * N l = N l) /\ (N l * N [] = N l)
    
     : goalstack

- e (RW_TAC list_ss [CONC_def]);       <font color="red">(* Expand first sub-goal by rewriting *)</font>
OK..

Goal proved.
|- (N [] * N l = N l) /\ (N l * N [] = N l)

Remaining subgoals:
> val it =
    (N [] * W l = W l) /\ (W l * N [] = W l)
    
     : goalstack

- e (RW_TAC list_ss [CONC_def]);      <font color="red">(* Expand second sub-goal by rewriting *)</font>
OK..

Goal proved.
|- (N [] * W l = W l) /\ (W l * N [] = W l)
> val it =
    Initial goal proved.
    |- (N [] * a = a) /\ (a * N [] = a) : goalstack
</pre></div>The proof below has the form:

 <font color="blue">val <i>theorem_name</i> = prove(<i>goal</i>,<i>tactic</i>)</font>

where <font color="blue"><i>tactic</i></font> uses the tactical <font color="blue">THEN</font> to combine the case-splitting
and rewriting tactics into a single tactic that does case analysis 
and then rewrites both the resulting goals.  </pre></div>*)

(*****************************************************************************)
(* We want to show that A is closed under *, that * is associative on A and  *)
(* that \epsilon is the identity for this operation.                         *)
(*****************************************************************************)
val CONC_identity =
 prove
  (``(N[] * a = a) /\ (a * N[] = a)``,
   Cases_on `a`
    THEN RW_TAC list_ss [CONC_def]);

(*<div class="comment"><pre>
The proof of <font color="blue">CONC_assoc</font> below case splits on <font color="blue">`a`</font>, <font color="blue">`b`</font> and <font color="blue">`c`</font>
(resulting in eight subgoals) followed by rewriting with the list
simplification set (<font color="blue">list_ss</font>) and the definition of <font color="blue">CONC</font>. 
</pre></div>*)

val CONC_assoc =
 prove
  (``a * (b * c) = (a * b) * c``,
   Cases_on `a` THEN Cases_on `b` THEN Cases_on `c`
    THEN RW_TAC list_ss [CONC_def]);

(*<div class="comment"><pre>
In the proof below (which is just by rewriting) we show <font color="blue">CONC</font>
satisfies the existing predicate <font color="blue">ASSOC</font>, which is defined in
<font color="blue">operatorTheory</font>. Since this theory has not been opened, we need to
use a 'long name' for <font color="blue">ASSOC_DEF</font>, namely <font color="blue">operatorTheory.ASSOC_DEF</font>.
<div class="session"><pre>
- operatorTheory.ASSOC_DEF;
> val it = |- !f. ASSOC f = !x y z. f x (f y z) = f (f x y) z : thm
</pre></div>Incidently, my convention is to append <font color="blue">_def</font> for definitions, but
other people append <font color="blue">_DEF</font> (or maybe don't append anything).  This is
just a 'house style' issue.
</pre></div>*)

val ASSOC_CONC =
 prove
  (``ASSOC $*``, 
   RW_TAC std_ss [operatorTheory.ASSOC_DEF,CONC_assoc]);

(*****************************************************************************)
(* for w \in N |w| is the number of elements in w, and |W(w)| = |w|          *)
(*****************************************************************************)

(*****************************************************************************)
(* Represent |w| by LEN w. HOL's built-in length function on lists           *)
(* is LENGTH.                                                                *)
(*****************************************************************************)
val LEN_def =
 Define
  `(LEN(N w) = LENGTH w) 
   /\
   (LEN(W w) = LENGTH w)`;

(*****************************************************************************)
(* we want to show that if w \in N then                                      *)
(* |w*v| = |w|+|v| and                                                       *)
(* |W(w)*v| = |w|                                                            *)
(*****************************************************************************)
val LEN =
 prove
  (``(LEN(N w * a) = LEN(N w) + LEN a)
     /\
     (LEN(W w * a) = LEN(W w))``,
   Cases_on `a`
    THEN RW_TAC list_ss [LEN_def,CONC_def]);

(*****************************************************************************)
(* We define (on A) w<=v (prefix) if there is u \in A such that w*u=v        *)
(*****************************************************************************)
val PREFIX_def = Define `PREFIX w v = ?u. w*u = v`;

val STRICT_PREFIX_def = Define `STRICT_PREFIX w v = PREFIX w v /\ ~(w = v)`;

(*****************************************************************************)
(* u<w   is u is prefix of w and u/=w                                        *)
(* One could try to prove that if u<w u is neutral                           *)
(*****************************************************************************)

val STRICT_PREFIX_NEUTRAL =
 prove
  (``STRICT_PREFIX u w ==> ?l. u = N l``,
   Cases_on `u` THEN Cases_on `w`
    THEN RW_TAC list_ss [STRICT_PREFIX_def,PREFIX_def,CONC_def]);

(*****************************************************************************)
(* We also define W(w)^k = w^k                                               *)
(*****************************************************************************)
val ELEM_def =
 Define
  `(ELEM (N l) n = EL n l) 
   /\
   (ELEM (W l) n = EL n l) `;

(*****************************************************************************)
(* The problem with fusion is that if w is a weak word that matches          *)
(* the beginning (but not the whole of) r1, then w should match r1:r2, so    *)
(* we need to see to it that the definition doesn't require that l matches   *)
(* the beginning of r2 in this case.                                         *)
(*                                                                           *)
(* This is the point of the end operator. We define for w \in N              *)
(*                                                                           *)
(*  end(w) = \epsilon                                                        *)
(*  end(W(w)) = W(\epsilon)                                                  *)
(*****************************************************************************)
val END_def =
 Define
  `(END(N w) = N[])
   /\
   (END(W w) = W[])`;

(*****************************************************************************)
(* Now we can use it to turn on/turn off words because                       *)
(*                                                                           *)
(* end(v)*w = w but                                                          *)
(* end(W(v))*w = W(\epsilon)                                                 *)
(*****************************************************************************)
val END =
 prove
  (``!v w. (END(N v) * w = w) /\ (END(W v) * w = W[])``,
   Cases_on `w`
    THEN RW_TAC list_ss [LEN_def,CONC_def,END_def]);


(*****************************************************************************)
(* We can now define tight satisfaction:                                     *)
(* w,v and u are finite neutral or weak words.                               *)
(* (definition below incorporates fusion from later message)                 *)
(*                                                                           *)
(* w|==. b     <=> w=\epsilon^- or (w \in N and |w|=1 and w^0||=b)           *)
(* w|==. r1;r2 <=>                                                           *)
(*        there exist v,u s.t. v*u=w and v|==. r1 and u|==.  r2              *)
(* w|==. r1:r2 <=>                                                           *)
(*        there exist v,u \in A and l s.t. v*l*u=w and v*l|==. r1            *)
(*                                          and end(v)*l*u|==.  r2           *)
(* w|==. r1&r2 <=> w|==. r1 and w|==.  r2                                    *)
(* w|==. r1|r2 <=> w|==. r1 or  w|==.  r2                                    *)
(* w|==. r*   <=> either w=\epsilon or there exists w1,w2,..wn such that     *)
(*                     w=*(w1w2..wn)=w1*w2*..*wn                             *)
(*                     and forall 1<=k<=n wk|==. r                           *)
(*****************************************************************************)

(*****************************************************************************)
(* Boolean expressions                                                       *)
(*****************************************************************************)
val bexp_def =
 Hol_datatype
  `bexp = B_PROP   of 'a                         (* atomic proposition       *)
        | B_NOT    of bexp                       (* negation                 *)
        | B_AND    of bexp # bexp`;              (* conjunction              *)

(*****************************************************************************)
(* B_SEM l b means "l |= b" where l is a letter, i.e. l : 'prop -> bool      *)
(*****************************************************************************)
val B_SEM_def =
 Define
  `(B_SEM l (B_PROP(p:'prop)) = p IN l)
   /\
   (B_SEM l (B_NOT b)         = ~(B_SEM l b))
   /\
   (B_SEM l (B_AND(b1,b2))    = B_SEM l b1 /\ B_SEM l b2)`;

(*****************************************************************************)
(* Syntax of Sequential Extended Regular Expressions (SEREs)                 *)
(*****************************************************************************)
val sere_def =
 Hol_datatype
  `sere = S_BOOL        of 'a bexp               (* boolean expression       *)
        | S_CAT         of sere # sere           (* r1 ;  r2                 *)
        | S_FUSION      of sere # sere           (* r1 :  r2                 *)
        | S_OR          of sere # sere           (* r1 |  r2                 *)
        | S_AND         of sere # sere           (* r1 && r2                 *)
        | S_REPEAT      of sere`;                (* r[*]                     *)

(*<div class="comment"><pre>
The proof of <font color="blue">sere_induct</font> below has the form:

 <font color="blue">val <i>ML name</i> = save_thm("<i>HOL name</i>",<i>forward proof</i></font>)

where <font color="blue">save_thm</font> saves a theorem, with name <font color="blue"><i>HOL name</i></font> in the database 
associated with the current theory, and returns the theorem (a value 
of ML type <font color="blue">thm</font>), which is bound here to <font color="blue"><i>ML name</font>.
</i>
The ML expression <font
color="blue"><i>forward proof</i></font>, when evaluated, performs Modus Ponens 
on the result of invoking a simplifier (<font color="blue">SIMP_RULE</font>) and a first-order reasoner 
(<font color="blue">PROVE</font>) and then generalises the variable <font color="blue">P</font>. We won't attempt 
more explanation here.

The theorem <font color="blue">sere_induct</font> is an induction theorem needed as a
parameter for the induction tactic <font color="blue">INDUCT_THEN</font> used later. The
automatically proved induction theorem is <font color="blue">TypeBase.induction_of "sere"</font>,
but this doesn't have the 'uncurried' form <font color="blue">INDUCT_THEN</font> needs. This
is a technical issue we won't explain here.  </pre></div>*)

(*****************************************************************************)
(* Structural induction rule for SEREs                                       *)
(*****************************************************************************)
val sere_induct = save_thm
  ("sere_induct",
   Q.GEN
    `P`
    (MATCH_MP
     (DECIDE ``(A ==> (B1 /\ B2)) ==> (A ==> B1)``)
     (SIMP_RULE
       std_ss
       [pairTheory.FORALL_PROD,
        PROVE[]``(!x y. P x ==> Q(x,y)) = !x. P x ==> !y. Q(x,y)``,
        PROVE[]``(!x y. P y ==> Q(x,y)) = !y. P y ==> !x. Q(x,y)``]
       (Q.SPECL
         [`P`,`\(r1,r2). P r1 /\ P r2`]
         (TypeBase.induction_of "sere")))));

(*****************************************************************************)
(* Some auxiliary definitions                                                *)
(*****************************************************************************)
val IS_WEAK_def   = Define `(IS_WEAK (W w)   = T) /\ (IS_WEAK (N w)   = F)`
and IS_NEUTRAL_def = Define `(IS_NEUTRAL (W w) = F) /\ (IS_NEUTRAL (N w) = T)`;

val IS_LETTER_def =
 Define
  `(IS_LETTER(N w) = ?l. w = [l])
   /\
   (IS_LETTER(W w) = ?l. w = [l])`;

(*****************************************************************************)
(* Semantics of SEREs                                                        *)
(*****************************************************************************)
val US_SEM_def =
 Define
  `(US_SEM v (S_BOOL b) = (IS_WEAK v   /\ (LEN v = 0))
                           \/ 
                          (IS_NEUTRAL v /\ (LEN v = 1) /\ B_SEM (ELEM v 0) b))
   /\
   (US_SEM v (S_CAT(r1,r2)) =
     ?v1 v2. (v = v1 * v2) /\ US_SEM v1 r1 /\ US_SEM v2 r2)
   /\
   (US_SEM v (S_FUSION(r1,r2)) =
     ?v1 v2 l. IS_LETTER l /\ (v = v1*l*v2)
               /\  
               US_SEM (v1*l) r1  /\ US_SEM (END(v1)*l*v2) r2)
   /\
   (US_SEM v (S_OR(r1,r2)) =
     US_SEM v r1 \/ US_SEM v r2)
   /\
   (US_SEM v (S_AND(r1,r2)) =
     US_SEM v r1 /\ US_SEM v r2)
   /\
   (US_SEM v (S_REPEAT r) =
     ?vlist. (v = FOLDL $* (N[]) vlist) /\ EVERY (\v. US_SEM v r) vlist)`;

(*<div class="comment"><pre>
The declaration of the ML variable <font color="blue">S_SEM_SIMP_TAC</font> just defines an
abbreviation for a tactic that rewrites with a bunch of definitions.

The tactical <font color="blue">THENL</font> is used to apply a different second tactic to
each of the subgoals generated by a first tactic: <font color="blue">T THEN [T1,T2,...,Tn]</font> 
first applies <font color="blue">T</font>, which must produce <font color="blue">n</font> subgoals; then tactic <font color="blue">Ti</font>
is applied to the <font color="blue">i</font>th subgoal.

Compare this with <font color="blue">T THEN T1</font> which first applied <font color="blue">T</font> and then applied
the same tactic, <font color="blue">T1</font> to any subgoals produced.
</pre></div>*)
val S_SEM_SIMP_TAC =
 RW_TAC list_ss [US_SEM_def,IS_WEAK_def,IS_NEUTRAL_def,LEN_def,ELEM_def];

(*<div class="comment"><pre>
In the proof of <font color="blue">TightTrueEmpty</font> below, the first step is to do
structural induction: this is invoked by the tactic 
<font color="blue">INDUCT_THEN sere_induct ASSUME_TAC</font>
<div class="session"><pre>
g ``!r. US_SEM (W[]) r``;
&lt;&lt;HOL message: inventing new type variable names: 'a>>
> val it =
    Proof manager status: 1 proof.
    1. Incomplete:
         Initial goal:
         !r. US_SEM (W []) r

     : proofs

- e (INDUCT_THEN sere_induct ASSUME_TAC);
OK..
6 subgoals:
> val it =
    US_SEM (W []) (S_REPEAT r)
    ------------------------------------
      US_SEM (W []) r
    
    US_SEM (W []) (S_AND (r,r'))
    ------------------------------------
      2.  US_SEM (W []) r
      1.  US_SEM (W []) r'
    
    US_SEM (W []) (S_OR (r,r'))
    ------------------------------------
      2.  US_SEM (W []) r
      1.  US_SEM (W []) r'
    
    US_SEM (W []) (S_FUSION (r,r'))
    ------------------------------------
      2.  US_SEM (W []) r
      1.  US_SEM (W []) r'
    
    US_SEM (W []) (S_CAT (r,r'))
    ------------------------------------
      2.  US_SEM (W []) r
      1.  US_SEM (W []) r'
    
    !b. US_SEM (W []) (S_BOOL b)
    
     : goalstack</pre></div>These 6 subgoals are then solved individually by the tactics shown
(the comments show which tactic solves which subgoal). For example,
the first subgoal is the one for <font color="blue">S_BOOL b</font>, which is solved
by the previously defined tactic <font color="blue">S_SEM_SIMP_TAC</font>. Continuing the session:
<div class="session"><pre>
e S_SEM_SIMP_TAC;
OK..

Goal proved.
|- !b. US_SEM (W []) (S_BOOL b)

Remaining subgoals:
> val it =
    US_SEM (W []) (S_REPEAT r)
    ------------------------------------
      US_SEM (W []) r
    
    US_SEM (W []) (S_AND (r,r'))
    ------------------------------------
      2.  US_SEM (W []) r
      1.  US_SEM (W []) r'
    
    US_SEM (W []) (S_OR (r,r'))
    ------------------------------------
      2.  US_SEM (W []) r
      1.  US_SEM (W []) r'
    
    US_SEM (W []) (S_FUSION (r,r'))
    ------------------------------------
      2.  US_SEM (W []) r
      1.  US_SEM (W []) r'
    
    US_SEM (W []) (S_CAT (r,r'))
    ------------------------------------
      2.  US_SEM (W []) r
      1.  US_SEM (W []) r'
     : goalstack
</pre></div>The second subgoal, the <font color="blue">S_CAT (r,r')</font> case, is solved by first applying 
<font color="blue">S_SEM_SIMP_TAC</font>:
<div class="session"><pre>
e S_SEM_SIMP_TAC;
OK..
1 subgoal:
> val it =
    ?v1 v2. (W [] = v1 * v2) /\ US_SEM v1 r /\ US_SEM v2 r'
    ------------------------------------
      2.  US_SEM (W []) r
      1.  US_SEM (W []) r'
     : goalstack
</pre></div>and then solving the resulting existentially-quantified goal by
supplying <font color="blue">`W []`</font> as witnesses for the two quantifiers, and then
simplifying (the <font color="blue">Q</font> in <font color="blue">Q.EXISTS_TAC</font> indicates that a singly quoted
term is required).<div class="session"><pre>
- e (Q.EXISTS_TAC `W []` THEN Q.EXISTS_TAC `W []`);
OK..
1 subgoal:
> val it =
    (W [] = W [] * W []) /\ US_SEM (W []) r /\ US_SEM (W []) r'
    ------------------------------------
      2.  US_SEM (W []) r
      1.  US_SEM (W []) r'
     : goalstack

- e (RW_TAC list_ss [CONC_def]);
OK..

Goal proved.
 [..] |- (W [] = W [] * W []) /\ US_SEM (W []) r /\ US_SEM (W []) r'

Goal proved.
 [..] |- ?v1 v2. (W [] = v1 * v2) /\ US_SEM v1 r /\ US_SEM v2 r'

Goal proved.
 [..] |- US_SEM (W []) (S_CAT (r,r'))

Remaining subgoals:
> val it =
    US_SEM (W []) (S_REPEAT r)
    ------------------------------------
      US_SEM (W []) r
    
    US_SEM (W []) (S_AND (r,r'))
    ------------------------------------
      2.  US_SEM (W []) r
      1.  US_SEM (W []) r'
    
    US_SEM (W []) (S_OR (r,r'))
    ------------------------------------
      2.  US_SEM (W []) r
      1.  US_SEM (W []) r'
    
    US_SEM (W []) (S_FUSION (r,r'))
    ------------------------------------
      2.  US_SEM (W []) r
      1.  US_SEM (W []) r'
     : goalstack</pre></div></pre></div>*)


(*****************************************************************************)
(* We can now prove with fusion in the language                              *)
(*   for all r: W(\espilon)|==.r                                             *)
(*****************************************************************************)
val TightTrueEmpty =
 prove
  (``!r. US_SEM (W[]) r``,
   INDUCT_THEN sere_induct ASSUME_TAC
    THENL
     [(* S_BOOL b *)
      S_SEM_SIMP_TAC,
      (* S_CAT (r,r') *)
      S_SEM_SIMP_TAC
       THEN Q.EXISTS_TAC `W []`
       THEN Q.EXISTS_TAC `W []`
       THEN RW_TAC list_ss [CONC_def],
      (* S_FUSION (r,r') *)
      S_SEM_SIMP_TAC
       THEN Q.EXISTS_TAC `W []`
       THEN Q.EXISTS_TAC `W []`
       THEN Q.EXISTS_TAC `W [b]`
       THEN RW_TAC list_ss [CONC_def,END,IS_LETTER_def],
      (* S_OR (r,r') *)
      S_SEM_SIMP_TAC,
      (* S_AND (r,r') *)
      S_SEM_SIMP_TAC,
      (* S_REPEAT (r,r') *)
      S_SEM_SIMP_TAC  
       THEN Q.EXISTS_TAC `[W []]`
       THEN RW_TAC list_ss [CONC_def]]);

(*****************************************************************************)
(* Weaken a word                                                             *)
(*****************************************************************************)
val WEAKEN_def = Define `(WEAKEN(N l) = W l) /\ (WEAKEN(W l) = W l)`;

val WEAKEN =
 prove
  (``(IS_WEAK(WEAKEN w) = T) /\ (IS_NEUTRAL(WEAKEN w) = F)``,
   Cases_on `w`
    THEN RW_TAC list_ss [IS_WEAK_def,IS_NEUTRAL_def,WEAKEN_def]);

val LEN_WEAKEN =
 prove
  (``LEN(WEAKEN w) = LEN w``,
   Cases_on `w`
    THEN RW_TAC list_ss [WEAKEN_def,LEN_def]);

(*<div class="comment"><pre>
The theorems that follow lead up to a proof of the Tight Prefix Theorem.
</pre></div>*)

(*****************************************************************************)
(* Tight prefix theorem                                                      *)
(* w|==.r and u&lt;w => W(u)|==.r                                               *)
(*****************************************************************************)
val APPEND_EQ_NIL =
 prove
  (``!l1 l2. (LENGTH(l1++l2) = 0) ==> (l1 = []) /\ (l2 = [])``,
   Induct 
    THEN RW_TAC list_ss [LENGTH_NIL]);

(*<div class="comment"><pre>
We'll go throught the proof of  <font color="blue">APPEND_EQ_SINGLETON</font> interactively. The session 
that follows is lightly edited. First we set up the goal and do induction.
<div class="session"><pre>
- g ``!l1 l2. (LENGTH(l1++l2) = 1) ==> (l1 = []) \/ (l2 = [])``;
&lt;&lt;HOL message: inventing new type variable names: 'a>>
> val it =
    Proof manager status: 1 proof.
    1. Incomplete:
         Initial goal:
         !l1 l2. (LENGTH (l1 ++ l2) = 1) ==> (l1 = []) \/ (l2 = [])

- e Induct;
OK..
2 subgoals:
> val it =
    !h l2. (LENGTH ((h::l1) ++ l2) = 1) ==> (h::l1 = []) \/ (l2 = [])
    ------------------------------------
      !l2. (LENGTH (l1 ++ l2) = 1) ==> (l1 = []) \/ (l2 = [])

    !l2. (LENGTH ([] ++ l2) = 1) ==> ([] = []) \/ (l2 = [])
</pre></div>The top subgoal (shown last) is solved just by rewriting.
<div class="session"><pre>
- e (RW_TAC list_ss []);
OK..

Goal proved.
|- !l2. (LENGTH ([] ++ l2) = 1) ==> ([] = []) \/ (l2 = [])

Remaining subgoals:
> val it =
    !h l2. (LENGTH ((h::l1) ++ l2) = 1) ==> (h::l1 = []) \/ (l2 = [])
    ------------------------------------
      !l2. (LENGTH (l1 ++ l2) = 1) ==> (l1 = []) \/ (l2 = [])
</pre></div>Next we simplify the remaining subgoal (the step case).
<div class="session"><pre>
- e (RW_TAC list_ss []);
OK..
1 subgoal:
> val it =
    l2 = []
    ------------------------------------
      2.  !l2. (LENGTH (l1 ++ l2) = 1) ==> (l1 = []) \/ (l2 = [])
      1.  LENGTH l2 + SUC (LENGTH l1) = 1
</pre></div>From assumption <font color="blue">1</font> it follows by arithmetic that <font color="blue">LENGTH l2 = 0</font>.
This can be established using <font color="blue">DECIDE_TAC</font> which is a Presburger arithmetic 
decision procedure. The tactic <font color="blue"><i>term</i> by <i>tactic</i></font> below (which uses 
the infix binary tactical <font color="blue">by</font>) attempts to prove <font color="blue"><i>term</i></font> from the current 
goal's assumptions using the tactic <font color="blue"><i>tactic</i></font>. 
If <font color="blue"><i>term</i></font> can be deduced, it is added to the assumptions.
<div class="session"><pre>
- e (`LENGTH l2 = 0` by DECIDE_TAC);
OK..
1 subgoal:
> val it =
    l2 = []
    ------------------------------------
      3.  !l2. (LENGTH (l1 ++ l2) = 1) ==> (l1 = []) \/ (l2 = [])
      2.  LENGTH l2 + SUC (LENGTH l1) = 1
      1.  LENGTH l2 = 0
</pre></div>Finally, we use <font color="blue">PROVE_TAC</font> (a heuristic first order reasoner) to
finish the proof.  We supply <font color="blue">|- !l. (LENGTH l = 0) = (l = [])</font>
(preproved and called <font color="blue">LENGTH_NIL</font>) as a parameter to <font color="blue">PROVE_TAC</font>.
<div class="session"><pre>
e (PROVE_TAC[LENGTH_NIL]);
OK..
Meson search level: ...

Goal proved.
 [...] |- l2 = []

Goal proved.
 [..] |- l2 = []

Goal proved.
 [.]
|- !h l2. (LENGTH ((h::l1) ++ l2) = 1) ==> (h::l1 = []) \/ (l2 = [])
> val it =
    Initial goal proved.
    |- !l1 l2. (LENGTH (l1 ++ l2) = 1) ==> (l1 = []) \/ (l2 = []) : goalstack</pre></div></pre></div>*)

val APPEND_EQ_SINGLETON =
 prove
  (``!l1 l2. (LENGTH(l1++l2) = 1) ==> (l1 = []) \/ (l2 = [])``,
   Induct 
    THEN RW_TAC list_ss []
    THEN `LENGTH l2 = 0` by DECIDE_TAC
    THEN PROVE_TAC[LENGTH_NIL]);

val APPEND_NIL_CANCEL =
 prove
  (``!l1 l2. (l1++l2 = l1) ==> (l2 = [])``,
   Induct 
    THEN RW_TAC list_ss []);

(*<div class="comment"><pre>
There are several simplification tactics in HOL. The most powerful is
<font color="blue">RW_TAC</font> which will automatically split up a goal into subgoals, and
invoke decision procedures. Less aggressive is <font color="blue">SIMP_TAC</font> which won't
decompose a goal, but just rewrites it. Both <font color="blue">RW_TAC</font> and <font color="blue">SIMP_TAC</font>
only rewrite the goal, but <font color="blue">FULL_SIMP_TAC</font>, which is used below,
rewrites both the goal and all the assumptions.</pre></div>*)
val PREFIX_CONC =
 prove
  (``PREFIX u v1 ==> !v2. PREFIX u (v1 * v2)``,
   Cases_on `u` THEN Cases_on `v1`
    THEN RW_TAC list_ss [PREFIX_def,CONC_def]
    THEN Cases_on `u` THEN Cases_on `v2`
    THEN FULL_SIMP_TAC list_ss [CONC_def,A_11,A_distinct]
    THENL
     [Q.EXISTS_TAC `N(l''++l''')`
       THEN RW_TAC list_ss [CONC_def],
      Q.EXISTS_TAC `W(l''++l''')`
       THEN RW_TAC list_ss [CONC_def]]);

(*****************************************************************************)
(* Not sure if this is needed                                                *)
(*****************************************************************************)
val STRICT_PREFIX_CONC =
 prove
  (``STRICT_PREFIX u v1 ==> !v2. STRICT_PREFIX u (v1 * v2)``,
   Cases_on `u` THEN Cases_on `v1`
    THEN RW_TAC list_ss [STRICT_PREFIX_def,PREFIX_def,CONC_def]
    THEN Cases_on `u` THEN Cases_on `v2`
    THEN FULL_SIMP_TAC list_ss [CONC_def,A_11,A_distinct]
    THENL
     [Q.EXISTS_TAC `N(l''++l''')`
       THEN RW_TAC list_ss [CONC_def],
      Q.EXISTS_TAC `W(l''++l''')`
       THEN RW_TAC list_ss [CONC_def],
      Cases_on `l = l' ++ l'''`
       THEN RW_TAC list_ss []
       THEN `l''' ++ l'' = []` by PROVE_TAC[APPEND_ASSOC,APPEND_NIL_CANCEL]
       THEN `(l''' = []) /\ (l'' = [])` by PROVE_TAC[APPEND_EQ_NIL,LENGTH_NIL]
       THEN RW_TAC list_ss []
       THEN FULL_SIMP_TAC list_ss []]);

val HD_APPEND =
 prove
  (``!v1 v2. ~(v1 = []) ==> (HD(APPEND v1 v2) = HD v1)``,
   Induct
    THEN RW_TAC list_ss []);

val TL_APPEND =
 prove
  (``!v1 v2. ~(v1 = []) ==> (TL(APPEND v1 v2) = APPEND (TL v1) v2)``,
   Induct
    THEN RW_TAC list_ss []);

val LIST_TRICHOTOMY_LEMMA1 =
 prove
  (``~(v = []) ==> (h::u ++ u' = v ++ v') ==> (h = HD v) /\ (u ++ u' = TL v ++ v')``,
   RW_TAC list_ss []
    THEN PROVE_TAC[HD,HD_APPEND,TL,TL_APPEND]);

(*<div class="comment"><pre>
<font color="blue">RES_TAC</font> combines pairs of assumptions to generate new assumptons
(which can then be used by subsequent tactics). It combines any pair
of assumptions of the form <font color="blue">A ==> B</font> and <font color="blue">A</font> to produce an additional
assumption <font color="blue">B</font> (it does more than this, including some pattern
matching).</pre></div>*)
val LIST_TRICHOTOMY_LEMMA2 =
 prove
  (``~(v = []) ==> (!w. ~(HD v::u ++ w = v)) ==> !w. ~(u ++ w = TL v)``,
   RW_TAC list_ss []
    THEN POP_ASSUM(ASSUME_TAC o SPEC_ALL)
    THEN Cases_on `~(u ++ w = TL v)`
    THEN FULL_SIMP_TAC list_ss []
    THEN `HD v :: u ++ w = HD v :: TL v` by PROVE_TAC[]
    THEN `~(NULL v)` by PROVE_TAC[NULL_EQ_NIL]
    THEN FULL_SIMP_TAC std_ss [CONS]
    THEN RES_TAC);

(*<div class="comment"><pre>
<font color="blue">IMP_RES_TAC <i>theorem</i></font>, where <font color="blue"><i>theorem</i></font> is an implication,
tries to use Modus Ponens and matching to derive consequences of
<font color="blue"><i>theorem</i></font> using assumptions as antecedents.</pre></div>*)
val LIST_TRICHOTOMY_LEMMA3 =
 prove
  (``!u v.
      (u ++ u' = v ++ v') /\ (!w. ~(u ++ w = v))
      ==>
      ?w. v ++ w = u``,
   Induct
    THEN RW_TAC list_ss []
    THEN Cases_on `v=[]`
    THEN RW_TAC list_ss []
    THEN IMP_RES_TAC LIST_TRICHOTOMY_LEMMA1
    THEN RW_TAC list_ss []
    THEN `TL(HD v::u ++ u') = TL(v ++ v')` by PROVE_TAC[]
    THEN FULL_SIMP_TAC list_ss []
    THEN IMP_RES_TAC LIST_TRICHOTOMY_LEMMA2
    THEN RES_TAC
    THEN `HD v :: TL v ++ w = HD v :: u` by PROVE_TAC[]
    THEN PROVE_TAC[APPEND,CONS,NULL_EQ_NIL]);

val LIST_TRICHOTOMY =
 prove
  (``!u v.
      (?u' v'. u ++ u'  = v ++ v')
      ==>
      (?w. u ++ w = v) \/ (?w. v ++ w = u)``,
   RW_TAC list_ss []
    THEN Cases_on `(?w. u ++ w = v)`  (* u<=v *)
    THEN RW_TAC list_ss []
    THEN FULL_SIMP_TAC list_ss []
    THEN Induct_on `u`
    THEN RW_TAC list_ss []
    THEN PROVE_TAC[LIST_TRICHOTOMY_LEMMA3,APPEND]);

(*<div class="comment"><pre>
<font color="blue">ZAP_TAC</font> combines <font color="blue">RW_TAC</font>-like rewriting with an invocation of <font color="blue">PROVE_TAC</font>,
Thus <font color="blue">ZAP_TAC <i>theorem list</i></font> is similar (though not identical) to:

   <font color="blue">RW_TAC std_ss <i>theorem list</i> THEN PROVE_TAC <i>theorem list</i></font>

(where <font color="blue">std_ss</font> is a standard simplification set).</pre></div>*)
val PREFIX_TRICHOTOMY =
 prove
  (``!v1 v2 w. 
       PREFIX v1 w /\ PREFIX v2 w ==> STRICT_PREFIX v1 v2 \/ PREFIX v2 v1``,
   Cases_on `v1` THEN Cases_on `v2` THEN Cases_on `w`
    THEN RW_TAC list_ss [PREFIX_def,STRICT_PREFIX_def,CONC_def]
    THEN Cases_on `u` THEN Cases_on `u'`
    THEN FULL_SIMP_TAC list_ss [PREFIX_def,STRICT_PREFIX_def,CONC_def,A_11,A_distinct]
    THEN Cases_on `?u. l' ++ u = l`
    THEN FULL_SIMP_TAC list_ss [PREFIX_def,STRICT_PREFIX_def,CONC_def,A_11,A_distinct]
    THEN ZAP_TAC list_ss [CONC_def,A_11]
    THEN Cases_on `?u. l++u = l'`
    THEN ZAP_TAC list_ss [CONC_def,A_11]
    THEN FULL_SIMP_TAC list_ss []
    THEN IMP_RES_TAC LIST_TRICHOTOMY
    THEN RES_TAC);

val PREFIX_REFL =
 prove
  (``!v. PREFIX v v``,
   Induct
    THEN RW_TAC list_ss [PREFIX_def,CONC_def]
    THEN Q.EXISTS_TAC `N[]`
    THEN RW_TAC list_ss [CONC_def]);

val APPEND_LEFT_CANCEL =
 store_thm
  ("APPEND_LEFT_CANCEL",
   ``(APPEND l l1 = APPEND l l2) = (l1 = l2)``,
   Induct_on `l`
    THEN ZAP_TAC list_ss []);

val PREFIX_CANCEL =
 prove
  (``(PREFIX (N(u ++ v1)) (N(u ++ v2)) ==> PREFIX (N v1) (N v2)) /\
     (PREFIX (W(u ++ v1)) (N(u ++ v2)) ==> PREFIX (W v1) (N v2)) /\
     (PREFIX (N(u ++ v1)) (W(u ++ v2)) ==> PREFIX (N v1) (W v2)) /\
     (PREFIX (W(u ++ v1)) (W(u ++ v2)) ==> PREFIX (W v1) (W v2))``,
   RW_TAC list_ss [PREFIX_def,CONC_def]
    THEN Cases_on `u'`
    THEN FULL_SIMP_TAC std_ss 
          [GSYM APPEND_ASSOC,CONC_def,A_11,A_distinct,APPEND_LEFT_CANCEL]
    THEN PROVE_TAC[CONC_def]);

val STRICT_PREFIX_CANCEL =
 prove
  (``(STRICT_PREFIX (N(u ++ v1)) (N(u ++ v2)) ==> STRICT_PREFIX (N v1) (N v2)) /\
     (STRICT_PREFIX (W(u ++ v1)) (N(u ++ v2)) ==> STRICT_PREFIX (W v1) (N v2)) /\
     (STRICT_PREFIX (N(u ++ v1)) (W(u ++ v2)) ==> STRICT_PREFIX (N v1) (W v2)) /\
     (STRICT_PREFIX (W(u ++ v1)) (W(u ++ v2)) ==> STRICT_PREFIX (W v1) (W v2))``,
   RW_TAC list_ss [STRICT_PREFIX_def]
    THEN PROVE_TAC[PREFIX_CANCEL]);

val B_FALSE_def =
 Define `B_FALSE = B_AND(B_PROP ARB, B_NOT(B_PROP ARB))`;

val B_FALSE =
 prove
  (``B_SEM v B_FALSE = F``,
   RW_TAC list_ss [B_FALSE_def,B_SEM_def]);

val IS_WEAK_LEN_0 =
 prove
  (``!v. IS_WEAK v /\ (LEN v = 0) = (v = W[])``,
   Induct
    THEN RW_TAC list_ss [IS_WEAK_def,LEN_def,LENGTH_NIL]);

val FOLDL_W_NIL =
 prove
  (``!l. ALL_EL (\v. v = W []) l ==> (FOLDL $* (W []) l = W[])``,
   Induct
    THEN RW_TAC list_ss [CONC_def]);

val FOLDL_N_NIL =
 prove
  (``!l. ~(l = []) ==> ALL_EL (\v. v = W []) l ==> (FOLDL $* (N []) l = W[])``,
   Induct
    THEN RW_TAC list_ss [CONC_def,FOLDL_W_NIL]);

val S_CATN_def =
 Define
  `(S_CATN 0 r = r) /\ (S_CATN (SUC n) r = S_CAT(r, S_CATN n r))`;

val ASSOC_FOLDL =
 prove
  (``!l x y. ASSOC f ==> (FOLDL f (f x y) l = f x (FOLDL f y l))``,
   Induct
    THEN RW_TAC list_ss [operatorTheory.ASSOC_DEF]);

val FOLDL_CONCAT_N =
 prove
  (``!vlist v. FOLDL $* v vlist = v * FOLDL $* (N []) vlist``,
   PROVE_TAC[ASSOC_FOLDL,ASSOC_CONC,CONC_identity]);

 val US_SEM_CAT_REPEAT_CATN =                      
  store_thm                                                                
   ("US_SEM_CAT_REPEAT_CATN",                                                  
    ``!v r. US_SEM v (S_CAT(S_REPEAT r, r)) = ?n. US_SEM v (S_CATN n r)``,
    RW_TAC list_ss [US_SEM_def]
     THEN EQ_TAC
     THEN RW_TAC list_ss []
     THENL                                                                 
      [Induct_on `vlist`
        THEN RW_TAC list_ss [CONC_identity,S_CATN_def,US_SEM_def]
        THEN ZAP_TAC std_ss [S_CATN_def]
        THEN RW_TAC std_ss []
        THEN RES_TAC
        THEN Q.EXISTS_TAC `SUC n` 
        THEN RW_TAC list_ss [S_CATN_def,US_SEM_def]
        THEN Q.EXISTS_TAC `h` THEN Q.EXISTS_TAC `FOLDL $* (N []) vlist * v2`
        THEN RW_TAC std_ss []
        THEN PROVE_TAC[FOLDL_CONCAT_N,CONC_assoc],
       Q.UNDISCH_TAC `US_SEM v (S_CATN n r)`
        THEN Q.SPEC_TAC(`v`,`v`)
        THEN Q.SPEC_TAC(`r`,`r`)
        THEN Q.SPEC_TAC(`n`,`n`)
        THEN Induct
        THEN RW_TAC list_ss [S_CATN_def]
        THENL                                                              
         [Q.EXISTS_TAC `N[]` THEN Q.EXISTS_TAC `v`
           THEN RW_TAC list_ss [CONC_identity]
           THEN Q.EXISTS_TAC `[]`
           THEN RW_TAC list_ss [],
          FULL_SIMP_TAC list_ss [US_SEM_def]
           THEN RES_TAC
           THEN RW_TAC std_ss []
           THEN Q.EXISTS_TAC `v1 * FOLDL $* (N []) vlist` THEN Q.EXISTS_TAC `v2'`
           THEN RW_TAC std_ss [CONC_assoc]
           THEN Q.EXISTS_TAC `v1::vlist`
           THEN RW_TAC list_ss [CONC_identity]
           THEN PROVE_TAC[FOLDL_CONCAT_N]]]);

val FOLDLN_def =
 Define
  `(FOLDLN 0 f e l = e) /\
   (FOLDLN (SUC n) f e l = FOLDLN n f (f e (HD l)) (TL l))`;

val FOLDLN_LENGTH =
 prove
  (``!l f e. FOLDLN (LENGTH l) f e l = FOLDL f e l``,
   Induct
    THEN RW_TAC list_ss [FOLDLN_def]);

val FOLDLN_ASSOC =
 prove
  (``!n v1 v2 l. FOLDLN n $* (v1 * v2) l = v1 * FOLDLN n $* v2 l``,
   Induct
    THEN RW_TAC list_ss [FOLDLN_def,CONC_assoc]);

val FOLDLN_CATN =
 prove
  (``!l v0 r.
      ALL_EL (\v. US_SEM v r) l /\ US_SEM v0 r 
      ==> 
      !n. n <= LENGTH l ==> US_SEM (FOLDLN n $* v0 l) (S_CATN n r)``,
   Induct
    THEN RW_TAC list_ss [FOLDLN_def,S_CATN_def]
    THEN Cases_on `n = 0`
    THEN RW_TAC list_ss [FOLDLN_def,S_CATN_def]
    THEN `?m. n = SUC m` by Cooper.COOPER_TAC
    THEN RW_TAC list_ss [FOLDLN_def,S_CATN_def]
    THEN FULL_SIMP_TAC arith_ss [US_SEM_def]
    THEN RES_TAC
    THEN Q.EXISTS_TAC `v0`
    THEN Q.EXISTS_TAC `FOLDLN m $* h l`
    THEN RW_TAC list_ss [FOLDLN_ASSOC]);

 val US_SEM_REPEAT_CATN =                      
  store_thm                                                                
   ("US_SEM_REPEAT_CATN",                                                  
    ``!v r. US_SEM v (S_REPEAT r) = (v = N[]) \/ ?n. US_SEM v (S_CATN n r)``,
    RW_TAC list_ss []
     THEN EQ_TAC
     THENL
      [SIMP_TAC list_ss[US_SEM_def]
        THEN REPEAT STRIP_TAC
        THEN Cases_on `v = N[]`
        THEN ASM_REWRITE_TAC[]
        THEN Cases_on `vlist`
        THEN FULL_SIMP_TAC list_ss [CONC_identity]
        THEN RES_TAC
        THEN `LENGTH t <= LENGTH t` by DECIDE_TAC
        THEN IMP_RES_TAC FOLDLN_CATN
        THEN Q.EXISTS_TAC `LENGTH t`
        THEN FULL_SIMP_TAC list_ss [FOLDLN_LENGTH],
       RW_TAC list_ss [US_SEM_def]
        THENL
         [Q.EXISTS_TAC `[]`
           THEN RW_TAC list_ss [],
          Q.UNDISCH_TAC `US_SEM v (S_CATN n r)`
           THEN Q.SPEC_TAC(`v`,`v`)
           THEN Q.SPEC_TAC(`r`,`r`)
           THEN Q.SPEC_TAC(`n`,`n`)
           THEN Induct
           THEN RW_TAC list_ss [S_CATN_def]
           THENL
            [Q.EXISTS_TAC `[v]`
              THEN RW_TAC list_ss [CONC_identity],
             FULL_SIMP_TAC list_ss [US_SEM_def]
              THEN RES_TAC
              THEN Q.EXISTS_TAC `v1::vlist`
              THEN RW_TAC list_ss [CONC_identity]
              THEN PROVE_TAC[FOLDL_CONCAT_N]]]]);

val WEAKEN_CONC =
 prove
  (``!v w. WEAKEN v * w = WEAKEN v``,
   Induct
    THEN RW_TAC list_ss [CONC_def,WEAKEN_def]);

val END_WEAKEN =
 prove
  (``!v. END(WEAKEN v) = W[]``,
   Induct
    THEN RW_TAC list_ss [CONC_def,WEAKEN_def,END_def]);

val NN_APPEND_PREFIX =
 prove
  (``!u v. PREFIX (N u) (N v) ==> PREFIX (N(w ++ u)) (N(w ++ v))``,
   RW_TAC list_ss [PREFIX_def,CONC_def]
    THEN Cases_on `u` THEN Cases_on `u'` THEN Cases_on `v` THEN Cases_on `w`
    THEN FULL_SIMP_TAC list_ss
          [CONC_def,CONC_identity,A_11,A_distinct]
    THENL
     [PROVE_TAC[CONC_identity],
      Q.EXISTS_TAC `N(h::t)`
       THEN RW_TAC list_ss [CONC_def],
      Q.EXISTS_TAC `N l`
       THEN RW_TAC std_ss [CONC_def,GSYM APPEND_ASSOC,APPEND],
      Q.EXISTS_TAC `N l`
       THEN RW_TAC std_ss [CONC_def,GSYM APPEND_ASSOC,APPEND]]);

val WN_APPEND_PREFIX =
 prove
  (``!u v. PREFIX (W u) (N v) ==> PREFIX (W(w ++ u)) (N(w ++ v))``,
   RW_TAC list_ss [PREFIX_def,CONC_def]
    THEN Cases_on `u` THEN Cases_on `u'` THEN Cases_on `v` THEN Cases_on `w`
    THEN FULL_SIMP_TAC list_ss
          [CONC_def,CONC_identity,A_11,A_distinct]);

val NW_APPEND_PREFIX =
 prove
  (``!u v. PREFIX (N u) (W v) ==> PREFIX (N(w ++ u)) (W(w ++ v))``,
   RW_TAC list_ss [PREFIX_def,CONC_def]
    THEN Cases_on `u` THEN Cases_on `u'` THEN Cases_on `v` THEN Cases_on `w`
    THEN FULL_SIMP_TAC list_ss
          [CONC_def,CONC_identity,A_11,A_distinct]
    THENL
     [Q.EXISTS_TAC `W[]`
       THEN RW_TAC list_ss [CONC_def],
      Q.EXISTS_TAC `W(h::t)`
       THEN RW_TAC list_ss [CONC_def],
      Q.EXISTS_TAC `W l`
       THEN RW_TAC std_ss [CONC_def,GSYM APPEND_ASSOC,APPEND],
      Q.EXISTS_TAC `W l`
       THEN RW_TAC std_ss [CONC_def,GSYM APPEND_ASSOC,APPEND]]);

val WW_APPEND_PREFIX =
 prove
  (``!u v. PREFIX (W u) (W v) ==> PREFIX (W(w ++ u)) (W(w ++ v))``,
   RW_TAC list_ss [PREFIX_def,CONC_def]
    THEN Cases_on `u` THEN Cases_on `u'` THEN Cases_on `v` THEN Cases_on `w`
    THEN FULL_SIMP_TAC list_ss
          [CONC_def,CONC_identity,A_11,A_distinct]);

val APPEND_STRICT_PREFIX =
 prove
  (``!u v.
      (STRICT_PREFIX (N u) (N v) ==> STRICT_PREFIX (N(w ++ u)) (N(w ++ v))) /\
      (STRICT_PREFIX (W u) (N v) ==> STRICT_PREFIX (W(w ++ u)) (N(w ++ v))) /\
      (STRICT_PREFIX (N u) (W v) ==> STRICT_PREFIX (N(w ++ u)) (W(w ++ v))) /\
      (STRICT_PREFIX (W u) (W v) ==> STRICT_PREFIX (W(w ++ u)) (W(w ++ v)))``,
   RW_TAC list_ss 
    [STRICT_PREFIX_def,
     NN_APPEND_PREFIX,WN_APPEND_PREFIX,NW_APPEND_PREFIX,WW_APPEND_PREFIX]);

val NOT_STRICT_PREFIX_N =
 prove
  (``!u. ~STRICT_PREFIX u (N [])``,
   Cases_on `u` 
    THEN RW_TAC list_ss [CONC_def,STRICT_PREFIX_def,PREFIX_def]
    THEN Cases_on `l = []`
    THEN RW_TAC list_ss [CONC_def]
    THEN Cases_on `u` 
    THEN RW_TAC list_ss [CONC_def,STRICT_PREFIX_def,PREFIX_def]);

val S_SEM_SIMPS =
  [US_SEM_def,IS_WEAK_def,IS_NEUTRAL_def,LEN_def,ELEM_def,
   WEAKEN_def,WEAKEN,LEN_WEAKEN,PREFIX_def,STRICT_PREFIX_def,CONC_def];

val TightPrefix_S_BOOL =
 prove
  (``!b w. 
      US_SEM w (S_BOOL b)
      ==>
      !u. STRICT_PREFIX u w ==> US_SEM (WEAKEN u) (S_BOOL b)``,
   RW_TAC list_ss S_SEM_SIMPS
    THEN Cases_on `u` THEN Cases_on `u'`
    THEN FULL_SIMP_TAC list_ss (S_SEM_SIMPS@[CONC_def,A_11,A_distinct])
    THEN `(LENGTH l = 0) \/ (LENGTH l' = 0)` by DECIDE_TAC
    THEN `l' = []` by PROVE_TAC[LENGTH_NIL]
    THEN FULL_SIMP_TAC list_ss []);

val TightPrefix_S_CAT =
 prove
  (``(!w. US_SEM w r ==> !u. STRICT_PREFIX u w ==> US_SEM (WEAKEN u) r) /\
     (!w. US_SEM w r' ==> !u. STRICT_PREFIX u w ==> US_SEM (WEAKEN u) r')
     ==>
     !w. US_SEM w (S_CAT (r,r')) 
         ==>
         !u. STRICT_PREFIX u w ==> US_SEM (WEAKEN u) (S_CAT (r,r'))``,
   RW_TAC list_ss [US_SEM_def]
    THEN Cases_on `STRICT_PREFIX u v1`
    THENL
     [RES_TAC
       THEN Q.EXISTS_TAC `WEAKEN u` THEN Q.EXISTS_TAC `v2`
       THEN RW_TAC list_ss []
       THEN Cases_on `u` THEN Cases_on `v2`
       THEN RW_TAC list_ss [WEAKEN_def,CONC_def],
      `PREFIX v1 u` by PROVE_TAC[PREFIX_TRICHOTOMY,STRICT_PREFIX_def,PREFIX_CONC,PREFIX_REFL]
       THEN FULL_SIMP_TAC list_ss [PREFIX_def]
       THEN Cases_on `v1` THEN Cases_on `v2` THEN Cases_on `u` THEN Cases_on `u'`
       THEN FULL_SIMP_TAC list_ss [WEAKEN_def,CONC_def,A_11,A_distinct]
       THEN Q.EXISTS_TAC`N l` THEN Q.EXISTS_TAC `W l'''`
       THEN RW_TAC list_ss [CONC_def]
       THEN IMP_RES_TAC STRICT_PREFIX_CANCEL
       THEN RES_TAC
       THEN FULL_SIMP_TAC list_ss [WEAKEN_def]]);

val TightPrefix_S_FUSION =
 prove
  (``(!w. US_SEM w r ==> !u. STRICT_PREFIX u w ==> US_SEM (WEAKEN u) r) /\
     (!w. US_SEM w r' ==> !u. STRICT_PREFIX u w ==> US_SEM (WEAKEN u) r')
     ==>
     !w. US_SEM w (S_FUSION (r,r')) 
         ==>
         !u. STRICT_PREFIX u w ==> US_SEM (WEAKEN u) (S_FUSION (r,r'))``,
   RW_TAC list_ss [US_SEM_def]
    THEN Cases_on `STRICT_PREFIX u (v1 * l)`
    THENL
     [`US_SEM (WEAKEN u) r` by PROVE_TAC[]
       THEN `US_SEM (WEAKEN u * l) r` by PROVE_TAC[WEAKEN_CONC]
       THEN `US_SEM (W[]) r'` by PROVE_TAC[TightTrueEmpty]
       THEN `US_SEM (END(WEAKEN u) * (l * v2)) r'` by RW_TAC list_ss [END_WEAKEN,CONC_def]
       THEN Q.EXISTS_TAC `WEAKEN u` THEN Q.EXISTS_TAC `v2` THEN Q.EXISTS_TAC `l`
       THEN RW_TAC list_ss []
       THEN Cases_on `u` 
       THEN RW_TAC list_ss [WEAKEN_def,CONC_def]
       THEN FULL_SIMP_TAC std_ss [CONC_assoc,WEAKEN_def],
      `PREFIX (v1 * l) u` by PROVE_TAC[PREFIX_TRICHOTOMY,STRICT_PREFIX_def,PREFIX_CONC,PREFIX_REFL]
       THEN FULL_SIMP_TAC list_ss [PREFIX_def]
       THEN Cases_on `v1` THEN Cases_on `v2` THEN Cases_on `u` THEN Cases_on `u'` THEN Cases_on `l`
       THEN FULL_SIMP_TAC list_ss [WEAKEN_def,CONC_def,A_11,A_distinct]
       THEN Q.EXISTS_TAC`N l'` THEN Q.EXISTS_TAC `W l''''` THEN Q.EXISTS_TAC `N l'''''` 
       THEN RW_TAC list_ss [CONC_def,END_def]
       THEN FULL_SIMP_TAC list_ss [CONC_def,END_def]
       THEN IMP_RES_TAC STRICT_PREFIX_CANCEL
       THEN PROVE_TAC[APPEND_STRICT_PREFIX,WEAKEN_def]]);

val TightPrefix_S_CATN =
 prove
  (``(!w. US_SEM w r ==> !u. STRICT_PREFIX u w ==> US_SEM (WEAKEN u) r) 
     ==>
     !n w. 
      US_SEM w (S_CATN n r) 
      ==>
      !u. STRICT_PREFIX u w ==> US_SEM (WEAKEN u) (S_CATN n r)``,
   DISCH_TAC
    THEN Induct
    THEN RW_TAC list_ss [S_CATN_def]
    THEN RES_TAC
    THEN IMP_RES_TAC TightPrefix_S_CAT);
 
val TightPrefix =
 prove
  (``!r w. US_SEM w r ==> !u. STRICT_PREFIX u w ==> US_SEM (WEAKEN u) r``,
   INDUCT_THEN sere_induct ASSUME_TAC
    THENL
     [(* S_BOOL b *)
      PROVE_TAC[TightPrefix_S_BOOL],
      (* S_CAT (r,r') *)
      RW_TAC std_ss []
       THEN IMP_RES_TAC TightPrefix_S_CAT,
      (* S_FUSION (r,r') *)
      RW_TAC std_ss []
       THEN IMP_RES_TAC TightPrefix_S_FUSION,
      (* S_OR (r,r') *)
      RW_TAC std_ss [US_SEM_def]
       THEN PROVE_TAC[],
      (* S_AND (r,r') *)
      RW_TAC std_ss [US_SEM_def]
       THEN PROVE_TAC[],
      (* S_REPEAT (r,r') *)
      PROVE_TAC[US_SEM_REPEAT_CATN,NOT_STRICT_PREFIX_N,TightPrefix_S_CATN]]);

(* 

<font color="red"><b>END OF FILE</b></font>
</pre>
</body>
</html>
*)